Modular program analyzers that exploit the program structure are more scalable since they avoid repeated analysis of program regions by computing reusable summaries. Traditional modular methods target proofs of program assertions by computing and composing summaries in an intertwined manner. For example, to compute a summary for a function F, the methods need to compute and compose the summaries of all the callees of F, even if many of these callees are irrelevant to checking the property at hand. Recent methods based on structural abstraction/refinement (SAR) alleviate this problem by dissociating summary composition from computation: function summaries and verification conditions are first computed locally by skipping the analysis of callees (abstraction phase) and then composed lazily with callee summaries (refinement phase). Refinement is property-driven and employs an efficient constraint solver for the program logic. In contrast to other abstraction/refinement methods, e.g., predicate abstraction, computing a structural abstraction is relatively inexpensive, and refinement is done incrementally via pre-computed function summaries.
SAR holds promise for scalable bug detection in software since the abstraction is inexpensive to compute and refinement employs pre-computed procedure summaries. The refinement step is key to the scalability of an SAR technique: efficient refinement should avoid exploring program regions irrelevant to the property being checked. Current refinement techniques, guided by the counterexamples obtained from constraint solvers, have little or no control over the program regions explored during refinement.
By dissociating summary computation from composition, SAR has the ability to select which regions to explore during the refinement (composition) phase for checking properties efficiently. The selective refinement strategy determines the efficiency of a SAR-based verification method. Ideally, we desire an optimal strategy, which explores (composes with) exactly those program regions which are relevant to a given property. Optimal refinement is as hard as the (undecidable) program verification problem since it may require a knowledge of the complete program behavior for making a selection. Consequently, researchers employ heuristics for performing refinement, guided by the counterexamples obtained when the solver checks the abstract model. However, the solver, being oblivious of the program structure, may produce spurious counterexamples that continuously drive the refinement towards exploring newer program regions, even though a witness may exist undetected in a subset of the currently explored regions. Redundant refinement of this form burdens the solver with irrelevant summary constraints, leading to dramatic increase in solving times, and, in many cases, to the failure of an SAR-based method.